FairFifo
== (i:Id, t:, l:IdLnk. ((source(l) = i))  (onlnk(l;m(i;t)) = []))
== & (i:Id, t:. (isnull(a(i;t)))  ((x:Id. s(i;t+1).x = (q.s(i;t).x(q + 1))) & m(i;t) = []))
== & ((i:Id, t:, l:IdLnk.
== & ((isrcv(l;a(i;t)))
== & ( (destination(l) = i & ((||queue(l;t)||  1 ) c (hd(queue(l;t)) = msg(a(i;t))))))
== & (c ((l:IdLnk, t:.
== & (c ((t':. ((t  t') & ((isrcv(l;a(destination(l);t')))  (queue(l;t') = []))))
== & (c & w-machine-constraint(w)
== & (c & w-atom-constraint(w)
== & (c & w-discrete-constraint(w))) 

latex

---

clarification:

fair-fifo{i:l}
fair-fifo(w)
== (i:Id, t:, l:IdLnk. ((source(l) = i  Id))  (onlnk(l;w-m(w; i; t)) = []  (w-Msg(w) List)))
== & (i:Id, t:.
== & ((w-isnull(w; w-a(w; i; t)))
== & ( ((x:Id. w-s(w; i; (t+1); x) = (q.w-s(w; i; t; x)(q + 1))  w-vartype(w; i; x))
== & ( & w-m(w; i; t) = []  (w-Msg(w) List)))
== & ((i:Id, t:, l:IdLnk.
== & ((w-isrcvl(w; l; w-a(w; i; t)))
== & ( (destination(l) = i  Id
== & ( & ((||w-queue(w; l; t)||  1 )
== & ( & (c (hd(w-queue(w; l; t)) = w-msg(w; w-a(w; i; t))  w-Msg(w)))))
== & (c ((l:IdLnk, t:.
== & (c ((t':
== & (c ((((t  t')
== & (c ((& ((w-isrcvl(w; l; w-a(w; destination(l); t')))
== & (c ((& ( (w-queue(w; l; t') = []  (w-Msg(w) List)))))
== & (c & w-machine-constraint(w)
== & (c & w-atom-constraint{i:l}
== & (c & w-atom-constraint(w)
== & (c & w-discrete-constraint(w))) 

latex

Definitions	A, source(l), onlnk(l;mss), isnull(a), x:AB(x), , vartype(i;x), n+m, x.A(x), f(a), s(i;t).x, r + s, m(i;t), P  Q, Id, A c B, i  j , ||as||, #$n, hd(l), msg(a), IdLnk, x:A. B(x), x:A. B(x), , A  B, P  Q, b, isrcv(l;a), a(i;t), destination(l), s = t, type List, Msg, queue(l;t), [], w-machine-constraint(w), P & Q, w-atom-constraint(w), w-discrete-constraint(w)
FDL editor aliases	fair-fifo